pnueli-zuck.10.jani:model: info: pnueli-zuck.10 is an MDP model.
pnueli-zuck.10.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.10.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.10.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.10.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.10.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.10.jani:variables[5]: info: Expanding variable "p5" into 16 locations in automaton "process5".
pnueli-zuck.10.jani:variables[6]: info: Expanding variable "p6" into 16 locations in automaton "process6".
pnueli-zuck.10.jani:variables[7]: info: Expanding variable "p7" into 16 locations in automaton "process7".
pnueli-zuck.10.jani:variables[8]: info: Expanding variable "p8" into 16 locations in automaton "process8".
pnueli-zuck.10.jani:variables[9]: info: Expanding variable "p9" into 16 locations in automaton "process9".
pnueli-zuck.10.jani: info: Need 24 bytes per state.
FRET called...
Peak memory usage: 60 MB
Analysis results for pnueli-zuck.10.jani
Property live
Probability: 1
Time: 0.0 s